$\forall$$T$, $A$:Type, $P$:($A$$\rightarrow$$T$$\rightarrow\mathbb{B}$), $k$:Knd, $i$, $r$, $x$:Id.
\\[0ex]Normal($T$)
\\[0ex]$\Rightarrow$ Normal($A$)
\\[0ex]$\Rightarrow$ ($\neg$($r$ = $x$))
\\[0ex]$\Rightarrow$ (($\uparrow$isrcv($k$)) $\Rightarrow$ ($i$ = destination(lnk($k$))))
\\[0ex]$\Rightarrow$ $\vdash$${\it es}$.recognizer{-}p(${\it es}$;$T$;$A$;$P$;$k$;$i$;$r$;$x$)